\section{Formal Framework For Property Preservation}\label{sec:operational_dref}

\subsection{Algebraic Petri Nets}

Algebraic Petri Nets are a formalism used for modeling, simulating and studying
the properties of concurrent systems. They are based on the well known
Place/Transition (P/T) Petri Nets formalism where \emph{places} hold resources
-- also known as tokens -- and \emph{transitions} are linked to places by
weighted input and output \emph{arcs}. The semantics of a
P/T Petri Net involves the sequential non-deterministic firing of transitions in the net
-- where firing a transition means consuming tokens from the set of places
linked to the input arcs of the transition and producing tokens into the set of
places linked to the output arcs of the transition. The algebraic extension
defines tokens as elements of sets (with associated operations) which
are models of algebraic specifications. The arcs of APNs can include weights
defined by terms of the algebraic specification and the transitions can be
guarded by algebraic equations.


% In this paper we propose using model checking as a means of verification of
% decidable properties on models. Model
% checking~\cite{Clarke:Emerson:1981,Queille:Sifakis:1982} is a technique widely
% used nowadays to verify if finite models satisfy properties expressed in
% temporal logics.
% Having this idea in mind, figure~\ref{fig:mono_res_mc} presents
% a fragment of three models $M_1$, $M_2$ and $M_3$ ordered from left to right,
% representing an evolving process. The property we wish the system to be resilient
% to is $C=p_1\land p_2\land p_3$ and the component properties that are
% not satisfied by each model are greyed out. Models $M_1$, $M_2$ and $M_3$
% exhibit monotonic resilience regarding $C$ because every model in the evolving
% system satisfies at least the same component properties of $C$ as the previous
% model in the evolving process.
% 
% Note that we have included in figure~\ref{fig:mono_res_mc} a set of artifacts
% called $CE_1$, $CE_2$ and $CE_3$ representing counterexamples produced by
% verifying properties that are not satisfied by the model. Counterexamples are artifacts
% produced by model checkers and provide information about parts of the model that
% violate the property being checked. Figure~\ref{fig:mono_res_mc} shows that this
% information can be used in order to help in deciding which kind of changes
% should be made to a model $M_k$ such that model $M_{k+1}$ might
% satisfy more component properties of $c$.
% 
% \begin{figure}[h!] \centering
% \includegraphics[scale=0.6]{images/resilience_model_checking.pdf}
% 	\caption{Monotonic Resilience using Model Checking}
% 	\label{fig:mono_res_mc}
% \end{figure}

\subsection{Extension of the Padberg/Gejewsky/Ermel Safety Preservation Theory for Algebraic Petri Nets}
\label{sec:safety_preserv_extension}

In this section we present the theory that poses the conditions
allowing the evolution of an APN model such that \emph{safety} properties are
preserved. Padberg, Gajewsky and Ermel have proposed in
~\cite{Padberg97refinementversus,Padberg98rule-basedrefinement} \emph{place
preserving} Algebraic High-Level (AHL) Net morphisms in order to preserve
\emph{safety properties}. Algebraic High-Level Nets are equivalent to the
Algebraic Petri Nets formalism we are using in the research presented in this
paper. Place preserving morphisms are a particular class of AHL net morphisms
mapping algebraic specifications, places, transitions and algebras. In the text
that follows we propose an extension to the theory presented
in~\cite{Padberg97refinementversus,Padberg98rule-basedrefinement} in order to
allow transition guard strengthening in a safety property place preserving
morphism. This extension is necessary in order to allow the kind of evolutions
we require for our evolving confidential filesystem example.

Definitions~\ref{def:AHL}, ~\ref{def:AHL_morph} and
theorem~\ref{th:safety_preserv} are simplified versions of the theory
presented in ~\cite{Padberg97refinementversus} and~\cite{Padberg98rule-basedrefinement}.
%They are provided at the necessary level of detail such that our
%extension can be understood.
The mathematical development in definitions~\ref{def:AHL_strenght} and
\ref{def:AHL_morph_strength}, lemma~\ref{th:mark_incl_strenght} and
proposition~\ref{th:safety_preserv_strength} consists an extension we propose in
order to allow transition guard strengthening during safety preserving evolution.

\begin{definition}{\textbf{Algebraic High-Level (AHL)}}
\label{def:AHL}

\emph{An Algebraic High-Level net is a 7-tuple $\langle SPEC,P,T,pre,post,cond,A
\rangle$ where $SPEC$ is an algebraic specification, $P$ is a set of places, $T$
a set of transitions, $pre$ and $post$ functions assigning term weighted input
and output arcs to transitions, $cond$ a function assigning a set of equational
conditions to transitions and $A$ an algebra which is model of $SPEC$.}
\end{definition}

\begin{definition}{\textbf{Place Preserving Algebraic High-Level Net Morphism}}
\label{def:AHL_morph} 

\emph{Let $N1=\langle
SPEC_1,P_1,T_1,pre_1,post_1,cond_1,A_1\rangle$ and $N2=\langle
SPEC_2,P_2,T_2,pre_2,post_2,cond_2,A_2\rangle$ be two AHL Nets.
$f=(f_P,f_T,f_{SPEC},f_A): N1\rightarrow N2$ is a \emph{Place Preserving} AHL
Net Morphism, where $f_P:P_1\rightarrow P_2$, $f_T:T_1\rightarrow T_2$,
$f_{SPEC}:SPEC_1\rightarrow SPEC_2$ and $f_A:A_1\rightarrow A_2$ are
morphisms, iff the following is true:
\begin{itemize}
  \item Firing conditions are preserved when transitions of $T_1$ are mapped
  onto $T_2$;
  \item Arcs adjacent to places of $P$ are preserved when those places are
  mapped onto the places of $P'$ by $f_p$;
  \item $f_T$, $f_P$ and $f_{SPEC}$ are injective and $f_{SPEC}$ is persistent, meaning
  the mapped signatures, terms and equations of $SPEC_1$ by $f_{SPEC}$ are
  contained in $SPEC_2$;
  \item There can be more places in the pre or post domain of a mapped
  transition than in the corresponding domains of the original transition;
  \item $A'$ merely extends the mapping of $A$ by $f_A$ for the new parts of
  $A'$ or it is merely renamed.
\end{itemize}}
\end{definition}

Let us now introduce the notions of strengthening the guards of a Algebraic
High-Level Net as well as the extension of the original place preserving AHL net
morphism in definition~\ref{def:AHL_morph} to include guard strengthening.

\begin{definition}{\textbf{Guard Strengthened Algebraic High-Level Net}}
\label{def:AHL_strenght}

\emph{Let $N1=\langle SPEC,P,T,pre,post,cond_1,A\rangle$ be an AHL. $N2=\langle
SPEC,P,T,pre,post,cond_2,A\rangle$ is a \emph{guard strengthened} version of $N$
if for all transitions $t\in T$ we have that $cond_1(t)\subseteq
cond_2(t)$\footnote{Note that there is an underlying AHL morphism between nets
$N1$ and its guard strengthened counterpart $N2$ which is in fact an isomorphism
if the new transition conditions in net $N2$ are excluded. For mathematical
simplification purposes we omit explicitly mentioning this morphism in our
text.}.}
\end{definition}

In other words, in definition~\ref{def:AHL_strenght} we consider that the
set of equations defining the conditions for transition $t$ of $N1$ is
syntactically included in the set of conditions for transition $t$ of $N2$. 

\begin{definition}{\textbf{Place Preserving Guard Strengthening Algebraic
High-Level Net Morphism}}
\label{def:AHL_morph_strength}

\emph{Let $N1$ and $N2$ be two AHL Nets and $f:N1\rightarrow N2$ be a place
preserving AHL Net morphism. $fs:N1\rightarrow N3$ is a place preserving \emph{guard
strengthening} AHL net morphism if there is a an AHL net $N3$ such that $N3$ is
a guard strengthened version of $N2$. $fs$ is the composition of AHL net
morphism $f$ with the implicit AHL net morphism mapping $N2$ into its guard
strengthened version $N3$.}
\end{definition}

We now present the original theorem that place preserving morphisms preserve
safety properties (proof in~\cite{Padberg97refinementversus}).

\begin{theorem}{\textbf{Place Preserving Morphisms Preserve Safety Properties}}
\label{th:safety_preserv}

\emph{Let $f:N1\rightarrow N2$ be a place preserving AHL net morphism and $M_1$
and $M_2$ be markings of $N_1$ and $N_2$ respectively, with $M_{2|f}=M_1$ (meaning
the restriction of the marking $M_2$ to $f_{M}(M_1)$\footnote{$f_{M}$ is the
extension of $f$ to markings.}). Let $\phi$ be a marking formula representing a
marking of the AHL network or formulas recursively built by the conjunction or
negation of marking formulas. Then there is the following equivalence:}

$$M_1\models_{N1}\square\phi \Leftrightarrow M_2\models_{N2}
\tau_f(\square\phi)$$

\emph{where $M\models_{N}\square\phi$ means formula $\phi$ is satisfied in all
markings attainable from marking $M$ by firing the transitions of AHL $N$. If we
consider only one marking $M$ of $N$, satisfaction of $\phi$ in $M$ means the
marking expressed in $\phi$ is contained in $M$. Finally, $\tau_f$ is the
function translating marking formulas regarding the \emph{place preserving} AHL
morphism $f$.}
\end{theorem}
\begin{proof}
See~\cite{Padberg97refinementversus}, theorem 3.17. 
\end{proof}

We start proving our main result by showing in
lemma~\ref{th:mark_incl_strenght} that adding guards to an AHL Net will not
introduce any new states in the reachable marking set of the original net. This
is so because adding guards will at most eliminate some of the states in the
original marking set.

\begin{lemma}{\textbf{Marking Inclusion Under Guard Strengthening}}
\label{th:mark_incl_strenght}
\end{lemma}
\begin{proof}
\emph{Let $N2$ be a \emph{guard strengthened} version of $N1$. We will show by
induction on the construction of the reachable markings of $N1$ and $N2$ that
the reachable markings of an APN $N2$ from a common initial marking $M$ are a
subset of the reachable markings of $N1$. The base case is trivial given that
$\{M\}\subseteq\{M\}$. For the inductive step let us assume that we have a set
of reachable markings $M_{N2}$ of $N2$ and a set of reachable markings $M_{N1}$
of $N1$ such that $M_{N2}\subseteq M_{N1}$. Then, given a common transition $t$
of both $N1$ and $N2$ three possibilities may happen: (1) $t$ is not enabled in
$N1$ and also not enabled in $N2$, which means the inclusion property keeps on
holding by hypothesis of the induction step ; (2) $t$ is enabled in $N1$ but not
in $N2$, which is the case that $t$ was strengthened in $N2$ (as per
definition~\ref{def:AHL_strenght}) and thus one more marking is produced for
$N1$ but not for $N2$. This means a new marking $M'$ is generated for $N1$ and
thus $M_{N2}\subseteq M_{N1}\cup\{M'\}$; and finally (3) $t$ is enabled for both
nets which means a common marking $M'$ is generated for both nets and
$M_{N2}\cup\{M'\} \subseteq M_{N1}\cup\{M'\}$.}
\end{proof}

We now prove in proposition~\ref{th:safety_preserv_strength} our main result.
The intuition behind the proof is the fact that the reachable marking set of a
strengthened net is a subset of the one of the safety preserving net, and as
such is still safe.

\begin{proposition}{\textbf{Place Preserving Guard Strengthening Morphisms
Preserve Safety Properties}}
\label{th:safety_preserv_strength}
\end{proposition}
\begin{proof}	
\emph{Let $fs:N1\rightarrow N2$ be a place preserving guard strengthening AHL
morphism. By definition~\ref{def:AHL_morph_strength} we know that there is a
place preserving AHL morphism $f:N1\rightarrow N3$ such that $N2$ is a guard
strengthened version of $N3$. By theorem~\ref{th:safety_preserv} we know that if
all markings of $N1$ satisfy a given safety formula $\phi$, then $\phi$'s image
$\tau(\phi)$ is satisfied by all the markings of $N3$. Then, by
proposition~\ref{th:mark_incl_strenght} we know the reachable markings of $N2$
are a subset of the reachable markings of $N3$. Since all the reachable markings
on $N3$ satisfy $\tau(\phi)$, so do all the markings of any of its subsets and
thus the proposition is proved.}
\end{proof}
